
\section{Discussion and Related Work}\label{sec:related_work}

Our preliminary concrete proposal for assisted model evolution raises many
questions. By researching the topic of assisted model evolution in a depth-first
fashion we have found a set of conditions under which certain kinds of dynamic
properties can be preserved during evolution. These conditions could be for
example used in a tool to enforce only certain kinds of changes to a model when
an evolution is required. The problem seems to be the fact that the evolution
conditions we found seem too restrictive to be generally applied. In fact, the
conditions we found present two main restrictions: (1) Given an evolution
$m\rightarrow m'$ (where $\{m,m'\}$ are APN models) we impose a structural
inclusion of $m$ into $m'$. (2) \emph{all} properties satisfied by a given model
should be preserved by any of its evolutions. The strength of these conditions
is no accident -- the preservation a model's semantics can become
meaningless when parts of a model are removed during evolution. Nonetheless, the
two conditions are applicable to evolution in particular domains, such as access control security.

Regarding point (1), while on the one hand our evolution conditions are very
taxing on the kind of evolutions that can happen, on the other hand they
guarantee that all safety properties verified by $m$ can are still expressible
and true in $m'$. If one would like to relax this evolution condition -- at the
risk of losing the meaning of the properties during evolution -- a possible path
would be to take into account the particular safety properties verified by $m$ when
evolving, which might lead to weaker conditions than the ones imposed by the
total \emph{place preserving} morphism we have introduced in
\Sect\ref{sec:prop_preserv_evol}. There is work from the model checking
community on alleviating state space explosion by simplifying specifications
using the variables in the properties under check. For example,
in~\cite{DBLP:conf/compos/BerezinCC97} the authors describe the \emph{cone of
reduction} technique used in hardware verification where a specification $P$ is
reduced in such a way that the reduced specification -- thus with a less
expensive state space -- $P'$ satisfies a formula $\phi$ if and only if $P$
satisfies $\phi$. More directly related to our research, in~\cite{rekow:2007} a
technique is presented for slicing Place/Transition Petri Nets with the goal of
easing the verification of LTL formulas. Both these pointers could be used in
our research for finding subnets of an APN model $m$ which satisfy a set of
safety properties such that the remaining part of $m$~can be discarded or
modified during evolution -- thus relaxing the \emph{place preserving} total
morphism constraint. Point (2) seems to be a variation of point 1) and could also
be tacked using the same techniques.

A final important question regarding the usage of \emph{safety properties} as a
means of representing requirements. Other types of properties could be envisaged
such as \emph{liveness}, \emph{reachability} or other properties expressible in
temporal logics. The preservation of such properties during evolution
imposes however other conditions which can be inspired
by~\cite{DBLP:conf/compos/BerezinCC97} and \cite{rekow:2007}. An
important step for the future is to match CTL property types with other types of
evolutions required in the real world for particular domains, which
requires additional and stronger real world case studies.